#include "PDTSMT2Visitor.h"

#include "PDTNode.h"
#include "PDTCodeGraph.h"
#include "PDTZ3GraphVisitor.h"
#include "PDTNumVar.h"
#include "PDTNumConst.h"
#include "PDTBoolVar.h"
#include "PDTBoolConst.h"
#include "PDTFunction.h"
#include "PDTProp.h"

const char * PDTSMT2Visitor::Z3Params = 
"(set-option PULL_NESTED_QUANTIFIERS true)\n"
"(set-option MODEL_COMPACT true)\n"
"(set-option MBQI true)\n"
"(set-option enable-cores)\n";


const char * PDTSMT2Visitor::declarations = 
"(declare-sort Statement 0)\n"
"\n"
"(declare-fun Start () Statement)      \n"
"(declare-fun Infinity ()  Statement)   \n"
"\n"
"(declare-sort Var 0)\n"
"(declare-fun IV (Var) Int)  \n"
";(define-fun IV ((v Var)) Int 0)\n"
"\n"
"(declare-fun E (Statement) Int)\n"
"(assert (= (E Start) 0))\n"
"(assert (< (E Start) (E Infinity)))\n"
"\n"
"(declare-fun eOrd0 (Statement Statement) Bool)\n"
"(define-fun eOrd0 ((s1 Statement) (s2 Statement)) Bool (< (E s1) (E s2)))\n"
"\n"
"(declare-fun inGamma0 (Var Statement) Bool)\n"
"\n"
"(declare-fun isMaxBefore (Var Statement Statement) Bool)\n"
"(define-fun isMaxBefore ((v Var) (sS Statement) (sT Statement)) Bool\n"
"          (and (< (E sT) (E Infinity))\n"
"               ( or (= sT Start) (inGamma0 v sT))\n"
"               (< (E sT) (E sS))\n"
"               (forall (s Statement) (=>                                \n"
"                      (inGamma0 v s)\n"
"                      (=> (< (E s) (E sS)) (<= (E s) (E sT)) ) )\n"
"                  :pattern ((inGamma0 v s) (< (E s) (E sS)))\n"
") ) )\n"
"\n"
"(declare-fun VAL (Var Int) Statement)                              \n"
"(assert (forall (s Statement) (v Var) \n"
"         (=> (and (> (E s) (E Start)) (<= (E s) (E Infinity)) ) \n"
"          (isMaxBefore v s (VAL v (E s))))))\n"
"\n"
"(declare-fun s2i (Statement) Int)\n"
"\n"
"(declare-fun Vs2i (Var Statement) Int)\n"
"(define-fun Vs2i ((v Var) (s Statement)) Int \n"
"  (ite (= s Start)             (IV v) (\n"
"  (ite (> (E s) (E Infinity)) 0 (\n"
"  (ite (= (VAL v (E s)) Start) (IV v) ( \n"
"                               s2i (VAL v (E s) ) ) ) ) ) ) ) )\n"
"\n"
"(assert (forall (v Var) \n"
"         (and \n"
"         (not (inGamma0 v Start)) (not (inGamma0 v Infinity)))))\n";

#if 0
; int x;
(declare-fun x () Var)

; int y;
(declare-fun y () Var)

;(assert (and (= (IV x) 0) (= (IV y) 0)))

;x=5;
(declare-fun s1 () Statement)
(assert (= (s2i s1) 5))
(assert (inGamma0 x s1))
(assert (not (inGamma0 y s1))) or 

(assert (forall (v Var) (=> (not (= v x)) (not (inGamma0 v s1)))))

(assert (eOrd0 Start s1))

;y= x + 1;
(declare-fun s2 () Statement)
(assert (= (s2i s2) (+ (Vs2i x s2) 1 )))
(assert (inGamma0 y s2))
(assert (not (inGamma0 x s2)))
(assert (eOrd0 s1 s2))

; x = y + 2
(declare-fun s3 () Statement)
(assert (= (s2i s3) (+ (Vs2i y s3) 2)))
(assert (inGamma0 x s3))
(assert (not (inGamma0 y s3)))
(assert (eOrd0 s2 s3))

(assert (eOrd0 s3 Infinity))

(assert (forall (s Statement) 
         (=> (distinct s Start s1 s2 s3 Infinity)
                       (<= (E Infinity) (E s)))))

(check-sat)
(get-unsat-core)
(model)
(echo "x(Start) x(s1) x(s2) x(s3) x(Infinity)")
(eval (Vs2i x Start) )
(eval (Vs2i x s1) )
(eval (Vs2i x s2))
(eval (Vs2i x s3))
(eval (Vs2i x Infinity))

(echo "y(Start) y(s1) y(s2) y(s3) y(Infinity)")
(eval (Vs2i y Start) )
(eval (Vs2i y s1) )
(eval (Vs2i y s2))
(eval (Vs2i y s3))
(eval (Vs2i y Infinity))
#endif

void
PDTSMT2Visitor::defineArraysOfStatements() {
#if 0

    const char * arrStatement [20];

    for (int i = 0; i < cg.depth; i++) {
        ss << "(define-sort A" << i+1 << "Statement (Array Int ";
        if (i == 0){
            ss << "Statement";
        } else {
            ss << "A" << i << "Statement";
        }
        ss << "))\n";
    }
#endif
}

/*
 Constructor of SMT2 Visitor
 */
PDTSMT2Visitor::
PDTSMT2Visitor(PDTCodeGraph & aCG) :
  counter(0), boundCounter(0), 
  ss(stringstream::in | stringstream::out),
    currentNode(NULL),
    cg(aCG)
{
#if 0
    ss << Z3Params << endl;
    ss << declarations << endl;

    arrStatement = new (const char *) [cg.depth+1];
    inGamma = new (const char * )[cg.depth+1];
    eOrd = new (const char *) [cg.depth+1];
    s2i = new (const char *) [cg.depth+1];

    for (int i = 0; i <= cg.depth; i++){
        arrStatement[i] = new char [20];
        inGamma[i] = new char [10];
        eOrd[i] = new char [10]; 
        s2i[i] = new char [10]; 
        if (i == 0){
            sprintf(arrStatement[0],"Statement");
        }else {
            sprintf(arrStatement[i],"A%dStatement", i);
        }
        sprintf(inGamma[i],"inGamma%d", i);
        sprintf(eOrd[i],"eOrd%d", i);
        sprintf(s2i[i],"s%s2i", i);
    }


    defineArraysOfStatements();

    //TODO: declare depth versions of the following
    //     1. Array of ... Statement
    //     2. inGamma-I-
    //     3. s-I-2i
    //     4. eOrd-I-
    for (int i = 0; i < cg.depth; i++) {
        ss << "(define-sort A" << i+1 << "Statement (Array Int ";
        if (i == 0){
            ss << "Statement";
        } else {
            ss << "A" << i << "Statement";
        }
        ss << "))\n";
    }


    // build Z3 nodes for variables and constants
    // start with them since they are at the bottom of
    // the parse DAG
    for (unsigned int i = 0; i < CG.variables.size(); i++)
    {
        //(declare-fun x () Var)
        PDTVar * var = cg.variables[i];
        ss << " (declare-fun " << var->getName() << " () Var)" << endl;
    }
#if 0
    for (unsigned int i = 0; i < CG.constants.size(); i++)
    {
        PDTNode * constant = cg.constants[i]->getNode();
        constant->SMT2visit(*this);
    }
#endif
    // visit all top nodes. 
    // that is all nodes with no parents.
    for (unsigned int i = 0; i < CG.nodes.size(); i++)
    {
        PDTNode * node = CG.nodes[i];

        /* taverse the top level nodes to keep track of the correct while depth */
        if (node->getParents().size() == 0)
            node->SMT2visit(*this);
    }
#endif
}

